Lean uses ++ (not +) for string/list concatenation because + carries an expectation of commutativity (a + b = b + a), while concatenation is explicitly non-commutative. Mixing the two notations would create confusion.

New pages

• TypeClass/Append.lean — homogeneous ++ operator class; explains the commutativity distinction with concrete examples:

  -- 文字列の連結は非可換: 順序が違うと結果が異なる
  #guard ("Hello, " ++ "world!" ≠ "world!" ++ "Hello, ")
  -- 一方、自然数の足し算は可換
  #guard 2 + 3 = 3 + 2

  Also shows a custom Append MyList instance and the internal expansion to HAppend.

• TypeClass/HAppend.lean — heterogeneous ++ operator class (parallel to existing HAdd/HMul); demonstrates custom HAppend (List Nat) Nat (List Nat) and the stdlib's HAppend (Array α) (List α) (Array α) instance.

Updated pages

• SUMMARY.lean — adds Append and HAppend in alphabetical order within the TypeClass section
• Type/String.lean, Type/List.lean — links Append instead of just mentioning the name inline